Inference at * 1 
Iof proof for Lemma fun thru spread:



1. A : Type
2. B : AType
3. p : x:A  B(x)
4. C : Type
5. D : Type
6. f : CD
7. b : x:AB(x)C
  f(let x,y = p in b(x,y)) = let x,y = p in f(b(x,y)) 

latex

 by ((New [`x';`y'] (D 3)) 
CollapseTHEN (AbReduce 0)) 

latex

C1: 

C1: 3. x : A
C1: 4. y : B(x)
C1: 5. C : Type
C1: 6. D : Type
C1: 7. f : CD
C1: 8. b : x:AB(x)C
C1:   f(b(x,y)) = f(b(x,y))
C.

Definitions

x:A  B(x)